ABSTRACT
We verify cryptographic protocols coded in C for correspondence properties with respect to the computational model of cryptography. The first step uses symbolic execution to extract a process calculus model from a C implementation of the protocol. The new contribution is the second step in which we translate the extracted model to a CryptoVerif protocol description, such that successful verification with CryptoVerif implies the security of the original C implementation. We implement our method and apply it to verify several protocols out of reach of previous work in the symbolic model (using ProVerif), either due to the use of XOR and Diffie-Hellman commitments, or due to the lack of an appropriate computational soundness result. We analyse only a single execution path, so our tool is limited to code following a fixed protocol narration. This is the first security analysis of C code to target a verifier for the computational model. We successfully verify over 3000 LOC. One example (about 1000 LOC) is independently written and currently in testing phase for industrial deployment; during its analysis we uncovered a vulnerability now fixed by its author.
- M. Abadi, B. Blanchet, and H. Comon-Lundh. Models and proofs of protocol security: A progress report. In A. Bouajjani and O. Maler, editors, CAV, volume 5643 of Lecture Notes in Computer Science, pages 35--49. Springer, 2009. Google ScholarDigital Library
- M. Abadi and P. Rogaway. Reconciling two views of cryptography (the computational soundness of formal encryption). J. Cryptology, 15(2):103--127, 2002.Google ScholarDigital Library
- M. Abe and V. D. Gligor, editors. Proceedings of the 2008 ACM Symposium on Information, Computer and Communications Security, ASIACCS 2008, Tokyo, Japan, March 18--20, 2008. ACM, 2008. Google ScholarCross Ref
- M. Aizatulin, F. Dupressoir, A. D. Gordon, and J. Jürjens. Verifying cryptographic code in C: Some experience and the Csec challenge. In Formal Aspects of Security and Trust (FAST 2011), Lecture Notes in Computer Science. Springer, 2011. Google ScholarDigital Library
- M. Aizatulin, A. D. Gordon, and J. Jürjens. Extracting and verifying cryptographic models from C protocol code by symbolic execution. In 18th ACM Conference on Computer and Communications Security (CCS 2011), 2011. Full version available at http://arxiv.org/abs/1107.1017. Google ScholarDigital Library
- M. Aizatulin, A. D. Gordon, and J. Jürjens. Computational verification of C protocol implementations by symbolic execution. Technical Report MSR-TR-2012-80, Microsoft Research, 2012.Google ScholarDigital Library
- M. Backes, D. Hofheinz, and D. Unruh. CoSP: A general framework for computational soundness proofs. In ACM Conference on Computer and Communications Security, pages 66--78, 2009. Preprint on IACR ePrint 2009/080. Google ScholarDigital Library
- M. Backes, M. Maffei, and D. Unruh. Computationally sound verification of source code. In CCS, 2010. Google ScholarDigital Library
- M. Barbosa, J. Pinto, J. Filliâtre, and B. Vieira. A deductive verification platform for cryptographic software. In Proceedings of the Fourth International Workshop on Foundations and Techniques for Open Source Software Certification (OpenCert 2010), volume 33 of Electronic Communications of the EASST. EASST, 2010.Google Scholar
- G. Barthe, B. Grégoire, S. Heraud, and S. Zanella Béguelin. Computer-aided security proofs for the working cryptographer. In Advances in Cryptology -- CRYPTO 2011, Lecture Notes in Computer Science. Springer, 2011. Google ScholarDigital Library
- J. Bengtson, K. Bhargavan, C. Fournet, A. D. Gordon, and S. Maffeis. Refinement types for secure implementations. In CSF '08: Proceedings of the 2008 21st IEEE Computer Security Foundations Symposium, pages 17--32. IEEE Computer Society, 2008. Google ScholarDigital Library
- K. Bhargavan, R. Corin, C. Fournet, and E. Zalinescu. Automated computational verification for cryptographic protocol implementations. Unpublished draft, Oct. 2009.Google Scholar
- K. Bhargavan, C. Fournet, R. Corin, and E. Zalinescu. Cryptographically verified implementations for TLS. In CCS '08: Proceedings of the 15th ACM conference on Computer and communications security, pages 459--468, Alexandria, VA, Oct. 2008. ACM. Google ScholarDigital Library
- K. Bhargavan, C. Fournet, and A. D. Gordon. Modular verification of security protocol code by typing. In ACM Symposium on Principles of Programming Languages (POPL'10), pages 445--456, 2010. Google ScholarDigital Library
- K. Bhargavan, C. Fournet, A. D. Gordon, and N. Swamy. Verified implementations of the information card federated identity-management protocol. In Abe and Gligor {3}, pages 123--135. Google ScholarDigital Library
- K. Bhargavan, C. Fournet, A. D. Gordon, and S. Tse. Verified interoperable implementations of security protocols. In CSFW '06: Proceedings of the 19th IEEE workshop on Computer Security Foundations, pages 139--152. IEEE Computer Society, 2006. Google ScholarDigital Library
- B. Blanchet. An efficient cryptographic protocol verifier based on prolog rules. In CSFW, pages 82--96. IEEE Computer Society, 2001. Google ScholarDigital Library
- B. Blanchet. Computationally sound mechanized proofs of correspondence assertions. In 20th IEEE Computer Security Foundations Symposium (CSF'07), pages 97--111, Venice, Italy, July 2007. IEEE. Google ScholarDigital Library
- B. Blanchet. A computationally sound mechanized prover for security protocols. IEEE Transactions on Dependable and Secure Computing, 5(4):193--207, Oct.-Dec. 2008. Google ScholarDigital Library
- B. Blanchet, A. D. Jaggard, A. Scedrov, and J.-K. Tsay. Computationally sound mechanized proofs for basic and public-key kerberos. In Abe and GligorciteDBLP:conf/ccs/2008asia, pages 87--99. Google ScholarDigital Library
- C. Cadar, D. Dunbar, and D. Engler. KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. In USENIX Symposium on Operating Systems Design and Implementation (OSDI 2008), San Diego, CA, Dec. 2008. Google ScholarDigital Library
- D. Cadé and B. Blanchet. From computationally-proved protocol specifications to implementations. In International Conference on Availability, Reliability and Security (ARES 2012), 2012. Google ScholarDigital Library
- S. Chaki and A. Datta. ASPIER: An automated framework for verifying security protocol implementations. In Computer Security Foundations Workshop, pages 172--185, 2009. Google ScholarDigital Library
- R. Corin and F. A. Manzano. Efficient symbolic execution for analysing cryptographic protocol implementations. In International Symposium on Engineering Secure Software and Systems (ESSOS'11), LNCS. Springer, 2011. Google ScholarDigital Library
- V. Cortier, S. Kremer, and B. Warinschi. A survey of symbolic methods in computational analysis of cryptographic systems. J. Autom. Reasoning, 46(3--4):225--259, 2011. Google ScholarDigital Library
- D. Dolev and A. Yao. On the Security of Public-Key Protocols. IEEE Transactions on Information Theory, 29(2):198--208, 1983. Google ScholarDigital Library
- F. Dupressoir, A. D. Gordon, J. Jürjens, and D. A. Naumann. Guiding a general-purpose C verifier to prove cryptographic protocols. In 24th IEEE Computer Security Foundations Symposium, 2011. Google ScholarDigital Library
- B. Dutertre and L. D. Moura. The Yices SMT Solver. Technical report, Computer Science Laboratory, SRI International, 2006.Google Scholar
- C. Fournet, K. Bhargavan, and A. D. Gordon. Cryptographic verification by typing for a sample protocol implementation. In Foundations of Security and Design VI (FOSAD 2010), Lecture Notes in Computer Science. Springer, 2011. To appear. Google ScholarDigital Library
- C. Fournet, M. Kohlweiss, and P.-Y. Strub. Modular code-based cryptographic verification. In 18th ACM Conference on Computer and Communications Security (CCS 2011), 2011. Google ScholarDigital Library
- http://frama-c.cea.fr/, 2009.Google Scholar
- P. Godefroid and S. Khurshid. Exploring very large state spaces using genetic algorithms. In Tools and Algorithms for Construction and Analysis of Systems (TACAS'02), volume 2280, pages 266--280. Springer, 2002. Google ScholarDigital Library
- P. Godefroid, N. Klarlund, and K. Sen. DART: directed automated random testing. In Programming Language Design and Implementation (PLDI'05), pages 213--223. ACM, 2005. Google ScholarDigital Library
- S. Goldwasser and S. Micali. Probabilistic encryption. Journal of Computer and System Science, 28(2):270--299, 1984.Google ScholarCross Ref
- A. D. Gordon. Provable implementations of security protocols. In LICS, pages 345--346, 2006. Google ScholarDigital Library
- J. Goubault-Larrecq and F. Parrennes. Cryptographic protocol analysis on real C code. In Proceedings of the 6th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'05), volume 3385 of Lecture Notes in Computer Science, pages 363--379. Springer, 2005. Google ScholarDigital Library
- P. Gupta and V. Shmatikov. Towards computationally sound symbolic analysis of key exchange protocols. In V. Atluri, P. Samarati, R. Küsters, and J. C. Mitchell, editors, FMSE, pages 23--32. ACM, 2005. Google ScholarDigital Library
- C. Hritcu. Union, Intersection, and Refinement Types and Reasoning About Type Disjointness for Security Protocol Analysis. PhD thesis, Department of Computer Science, Saarland University, 2011.Google Scholar
- A. Jeffrey and R. Ley-Wild. Dynamic model checking of C cryptographic protocol implementations. In Proceedings of Workshop on Foundations of Computer Security and Automated Reasoning for Security Protocol Analysis, 2006.Google Scholar
- J. C. King. Symbolic execution and program testing. Commun. ACM, 19(7):385--394, 1976. Google ScholarDigital Library
- R. Küsters and T. Truderung. Reducing protocol analysis with XOR to the XOR-free case in the horn theory based approach. Journal of Automated Reasoning, 46(3):325--352, 2011. Google ScholarDigital Library
- R. Küsters, T. Truderung, and J. Graf. A Framework for the Cryptographic Verification of Java-like Programs. In IEEE Computer Security Foundations Symposium, CSF 2012. IEEE Computer Society, 2012. Google ScholarDigital Library
- R. Küsters and M. Tuengerthal. Computational soundness for key exchange protocols with symmetric encryption. In E. Al-Shaer, S. Jha, and A. D. Keromytis, editors, ACM Conference on Computer and Communications Security, pages 91--100. ACM, 2009. Google ScholarDigital Library
- P. Lincoln, J. C. Mitchell, M. Mitchell, and A. Scedrov. Probabilistic polynomial-time equivalence and security analysis. In J. M. Wing, J. Woodcock, and J. Davies, editors, World Congress on Formal Methods, volume 1708 of Lecture Notes in Computer Science, pages 776--793. Springer, 1999. Google ScholarDigital Library
- G. C. Necula, S. McPeak, S. P. Rahul, and W. Weimer. CIL: Intermediate Language and Tools for Analysis and Transformation of C Programs. In Proceedings of the 11th International Conference on Compiler Construction, CC '02, pages 213--228, London, UK, 2002. Springer-Verlag. Google ScholarDigital Library
- PolarSSL. http://polarssl.org.Google Scholar
- N. Polikarpova and M. Moskal. Verifying implementations of security protocols by refinement. In Verified Software: Theories, Tools and Experiments (VSTTE 2012), volume 7152 of Lecture Notes in Computer Science, pages 50--65. Springer, 2012. Google ScholarDigital Library
- Project EVA. Security protocols open repository, 2007. http://www.lsv.ens-cachan.fr/spore/.Google Scholar
- A. Rial and G. Danezis. Privacy-friendly smart metering. Technical Report MSR-TR-2010-150, Microsoft Research, 2010.Google Scholar
- O. Udrea, C. Lumezanu, and J. S. Foster. Rule-Based static analysis of network protocol implementations. IN PROCEEDINGS OF THE 15TH USENIX SECURITY SYMPOSIUM, pages 193--208, 2006. Google ScholarDigital Library
- D. Unruh. The impossibility of computationally sound XOR, July 2010. Preprint on IACR ePrint 2010/389.Google Scholar
Index Terms
- Computational verification of C protocol implementations by symbolic execution
Recommendations
Extracting and verifying cryptographic models from C protocol code by symbolic execution
CCS '11: Proceedings of the 18th ACM conference on Computer and communications securityConsider the problem of verifying security properties of a cryptographic protocol coded in C. We propose an automatic solution that needs neither a pre-existing protocol description nor manual annotation of source code. First, symbolically execute the C ...
A cryptographically sound security proof of the Needham-Schroeder-Lowe public-key protocol
We present a cryptographically sound security proof of the well-known Needham-Schroeder-Lowe public-key protocol for entity authentication. This protocol was previously only proved over unfounded abstractions from cryptography. We show that it is secure ...
Protocol Verification via Projections
The method of projections is a new approach to reduce the complexity of analyzing nontrivial communication protocols. A protocol system consists of a network of protocol entities and communication channels. Protocol entities interact by exchanging ...
Comments